Left Termination of the query pattern convert(b,b,f) w.r.t. the given Prolog program could successfully be proven:



↳ PROLOG
  ↳ PrologToPiTRSProof

convert3({}0, B, 00).
convert3(.2(00, XS), B, X) :- convert3(XS, B, Y), times3(Y, B, X).
convert3(.2(s1(Y), XS), B, s1(X)) :- convert3(.2(Y, XS), B, X).
plus3(00, Y, Y).
plus3(s1(X), Y, s1(Z)) :- plus3(X, Y, Z).
times3(00, Y, 00).
times3(s1(X), Y, Z) :- times3(X, Y, U), plus3(Y, U, Z).


With regard to the inferred argument filtering the predicates were used in the following modes:
convert3: (b,b,f)
times3: (b,b,f)
plus3: (b,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:


convert_3_in_gga3([]_0, B, 0_0) -> convert_3_out_gga3([]_0, B, 0_0)
convert_3_in_gga3(._22(0_0, XS), B, X) -> if_convert_3_in_1_gga4(XS, B, X, convert_3_in_gga3(XS, B, Y))
convert_3_in_gga3(._22(s_11(Y), XS), B, s_11(X)) -> if_convert_3_in_3_gga5(Y, XS, B, X, convert_3_in_gga3(._22(Y, XS), B, X))
if_convert_3_in_3_gga5(Y, XS, B, X, convert_3_out_gga3(._22(Y, XS), B, X)) -> convert_3_out_gga3(._22(s_11(Y), XS), B, s_11(X))
if_convert_3_in_1_gga4(XS, B, X, convert_3_out_gga3(XS, B, Y)) -> if_convert_3_in_2_gga5(XS, B, X, Y, times_3_in_gga3(Y, B, X))
times_3_in_gga3(0_0, Y, 0_0) -> times_3_out_gga3(0_0, Y, 0_0)
times_3_in_gga3(s_11(X), Y, Z) -> if_times_3_in_1_gga4(X, Y, Z, times_3_in_gga3(X, Y, U))
if_times_3_in_1_gga4(X, Y, Z, times_3_out_gga3(X, Y, U)) -> if_times_3_in_2_gga5(X, Y, Z, U, plus_3_in_gga3(Y, U, Z))
plus_3_in_gga3(0_0, Y, Y) -> plus_3_out_gga3(0_0, Y, Y)
plus_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_plus_3_in_1_gga4(X, Y, Z, plus_3_in_gga3(X, Y, Z))
if_plus_3_in_1_gga4(X, Y, Z, plus_3_out_gga3(X, Y, Z)) -> plus_3_out_gga3(s_11(X), Y, s_11(Z))
if_times_3_in_2_gga5(X, Y, Z, U, plus_3_out_gga3(Y, U, Z)) -> times_3_out_gga3(s_11(X), Y, Z)
if_convert_3_in_2_gga5(XS, B, X, Y, times_3_out_gga3(Y, B, X)) -> convert_3_out_gga3(._22(0_0, XS), B, X)

The argument filtering Pi contains the following mapping:
convert_3_in_gga3(x1, x2, x3)  =  convert_3_in_gga2(x1, x2)
[]_0  =  []_0
0_0  =  0_0
._22(x1, x2)  =  ._22(x1, x2)
s_11(x1)  =  s_11(x1)
convert_3_out_gga3(x1, x2, x3)  =  convert_3_out_gga1(x3)
if_convert_3_in_1_gga4(x1, x2, x3, x4)  =  if_convert_3_in_1_gga2(x2, x4)
if_convert_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_convert_3_in_3_gga1(x5)
if_convert_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_convert_3_in_2_gga1(x5)
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga2(x2, x4)
if_times_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_2_gga1(x5)
plus_3_in_gga3(x1, x2, x3)  =  plus_3_in_gga2(x1, x2)
plus_3_out_gga3(x1, x2, x3)  =  plus_3_out_gga1(x3)
if_plus_3_in_1_gga4(x1, x2, x3, x4)  =  if_plus_3_in_1_gga1(x4)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

convert_3_in_gga3([]_0, B, 0_0) -> convert_3_out_gga3([]_0, B, 0_0)
convert_3_in_gga3(._22(0_0, XS), B, X) -> if_convert_3_in_1_gga4(XS, B, X, convert_3_in_gga3(XS, B, Y))
convert_3_in_gga3(._22(s_11(Y), XS), B, s_11(X)) -> if_convert_3_in_3_gga5(Y, XS, B, X, convert_3_in_gga3(._22(Y, XS), B, X))
if_convert_3_in_3_gga5(Y, XS, B, X, convert_3_out_gga3(._22(Y, XS), B, X)) -> convert_3_out_gga3(._22(s_11(Y), XS), B, s_11(X))
if_convert_3_in_1_gga4(XS, B, X, convert_3_out_gga3(XS, B, Y)) -> if_convert_3_in_2_gga5(XS, B, X, Y, times_3_in_gga3(Y, B, X))
times_3_in_gga3(0_0, Y, 0_0) -> times_3_out_gga3(0_0, Y, 0_0)
times_3_in_gga3(s_11(X), Y, Z) -> if_times_3_in_1_gga4(X, Y, Z, times_3_in_gga3(X, Y, U))
if_times_3_in_1_gga4(X, Y, Z, times_3_out_gga3(X, Y, U)) -> if_times_3_in_2_gga5(X, Y, Z, U, plus_3_in_gga3(Y, U, Z))
plus_3_in_gga3(0_0, Y, Y) -> plus_3_out_gga3(0_0, Y, Y)
plus_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_plus_3_in_1_gga4(X, Y, Z, plus_3_in_gga3(X, Y, Z))
if_plus_3_in_1_gga4(X, Y, Z, plus_3_out_gga3(X, Y, Z)) -> plus_3_out_gga3(s_11(X), Y, s_11(Z))
if_times_3_in_2_gga5(X, Y, Z, U, plus_3_out_gga3(Y, U, Z)) -> times_3_out_gga3(s_11(X), Y, Z)
if_convert_3_in_2_gga5(XS, B, X, Y, times_3_out_gga3(Y, B, X)) -> convert_3_out_gga3(._22(0_0, XS), B, X)

The argument filtering Pi contains the following mapping:
convert_3_in_gga3(x1, x2, x3)  =  convert_3_in_gga2(x1, x2)
[]_0  =  []_0
0_0  =  0_0
._22(x1, x2)  =  ._22(x1, x2)
s_11(x1)  =  s_11(x1)
convert_3_out_gga3(x1, x2, x3)  =  convert_3_out_gga1(x3)
if_convert_3_in_1_gga4(x1, x2, x3, x4)  =  if_convert_3_in_1_gga2(x2, x4)
if_convert_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_convert_3_in_3_gga1(x5)
if_convert_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_convert_3_in_2_gga1(x5)
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga2(x2, x4)
if_times_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_2_gga1(x5)
plus_3_in_gga3(x1, x2, x3)  =  plus_3_in_gga2(x1, x2)
plus_3_out_gga3(x1, x2, x3)  =  plus_3_out_gga1(x3)
if_plus_3_in_1_gga4(x1, x2, x3, x4)  =  if_plus_3_in_1_gga1(x4)


Pi DP problem:
The TRS P consists of the following rules:

CONVERT_3_IN_GGA3(._22(0_0, XS), B, X) -> IF_CONVERT_3_IN_1_GGA4(XS, B, X, convert_3_in_gga3(XS, B, Y))
CONVERT_3_IN_GGA3(._22(0_0, XS), B, X) -> CONVERT_3_IN_GGA3(XS, B, Y)
CONVERT_3_IN_GGA3(._22(s_11(Y), XS), B, s_11(X)) -> IF_CONVERT_3_IN_3_GGA5(Y, XS, B, X, convert_3_in_gga3(._22(Y, XS), B, X))
CONVERT_3_IN_GGA3(._22(s_11(Y), XS), B, s_11(X)) -> CONVERT_3_IN_GGA3(._22(Y, XS), B, X)
IF_CONVERT_3_IN_1_GGA4(XS, B, X, convert_3_out_gga3(XS, B, Y)) -> IF_CONVERT_3_IN_2_GGA5(XS, B, X, Y, times_3_in_gga3(Y, B, X))
IF_CONVERT_3_IN_1_GGA4(XS, B, X, convert_3_out_gga3(XS, B, Y)) -> TIMES_3_IN_GGA3(Y, B, X)
TIMES_3_IN_GGA3(s_11(X), Y, Z) -> IF_TIMES_3_IN_1_GGA4(X, Y, Z, times_3_in_gga3(X, Y, U))
TIMES_3_IN_GGA3(s_11(X), Y, Z) -> TIMES_3_IN_GGA3(X, Y, U)
IF_TIMES_3_IN_1_GGA4(X, Y, Z, times_3_out_gga3(X, Y, U)) -> IF_TIMES_3_IN_2_GGA5(X, Y, Z, U, plus_3_in_gga3(Y, U, Z))
IF_TIMES_3_IN_1_GGA4(X, Y, Z, times_3_out_gga3(X, Y, U)) -> PLUS_3_IN_GGA3(Y, U, Z)
PLUS_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> IF_PLUS_3_IN_1_GGA4(X, Y, Z, plus_3_in_gga3(X, Y, Z))
PLUS_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> PLUS_3_IN_GGA3(X, Y, Z)

The TRS R consists of the following rules:

convert_3_in_gga3([]_0, B, 0_0) -> convert_3_out_gga3([]_0, B, 0_0)
convert_3_in_gga3(._22(0_0, XS), B, X) -> if_convert_3_in_1_gga4(XS, B, X, convert_3_in_gga3(XS, B, Y))
convert_3_in_gga3(._22(s_11(Y), XS), B, s_11(X)) -> if_convert_3_in_3_gga5(Y, XS, B, X, convert_3_in_gga3(._22(Y, XS), B, X))
if_convert_3_in_3_gga5(Y, XS, B, X, convert_3_out_gga3(._22(Y, XS), B, X)) -> convert_3_out_gga3(._22(s_11(Y), XS), B, s_11(X))
if_convert_3_in_1_gga4(XS, B, X, convert_3_out_gga3(XS, B, Y)) -> if_convert_3_in_2_gga5(XS, B, X, Y, times_3_in_gga3(Y, B, X))
times_3_in_gga3(0_0, Y, 0_0) -> times_3_out_gga3(0_0, Y, 0_0)
times_3_in_gga3(s_11(X), Y, Z) -> if_times_3_in_1_gga4(X, Y, Z, times_3_in_gga3(X, Y, U))
if_times_3_in_1_gga4(X, Y, Z, times_3_out_gga3(X, Y, U)) -> if_times_3_in_2_gga5(X, Y, Z, U, plus_3_in_gga3(Y, U, Z))
plus_3_in_gga3(0_0, Y, Y) -> plus_3_out_gga3(0_0, Y, Y)
plus_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_plus_3_in_1_gga4(X, Y, Z, plus_3_in_gga3(X, Y, Z))
if_plus_3_in_1_gga4(X, Y, Z, plus_3_out_gga3(X, Y, Z)) -> plus_3_out_gga3(s_11(X), Y, s_11(Z))
if_times_3_in_2_gga5(X, Y, Z, U, plus_3_out_gga3(Y, U, Z)) -> times_3_out_gga3(s_11(X), Y, Z)
if_convert_3_in_2_gga5(XS, B, X, Y, times_3_out_gga3(Y, B, X)) -> convert_3_out_gga3(._22(0_0, XS), B, X)

The argument filtering Pi contains the following mapping:
convert_3_in_gga3(x1, x2, x3)  =  convert_3_in_gga2(x1, x2)
[]_0  =  []_0
0_0  =  0_0
._22(x1, x2)  =  ._22(x1, x2)
s_11(x1)  =  s_11(x1)
convert_3_out_gga3(x1, x2, x3)  =  convert_3_out_gga1(x3)
if_convert_3_in_1_gga4(x1, x2, x3, x4)  =  if_convert_3_in_1_gga2(x2, x4)
if_convert_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_convert_3_in_3_gga1(x5)
if_convert_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_convert_3_in_2_gga1(x5)
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga2(x2, x4)
if_times_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_2_gga1(x5)
plus_3_in_gga3(x1, x2, x3)  =  plus_3_in_gga2(x1, x2)
plus_3_out_gga3(x1, x2, x3)  =  plus_3_out_gga1(x3)
if_plus_3_in_1_gga4(x1, x2, x3, x4)  =  if_plus_3_in_1_gga1(x4)
IF_TIMES_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_TIMES_3_IN_1_GGA2(x2, x4)
IF_TIMES_3_IN_2_GGA5(x1, x2, x3, x4, x5)  =  IF_TIMES_3_IN_2_GGA1(x5)
IF_CONVERT_3_IN_3_GGA5(x1, x2, x3, x4, x5)  =  IF_CONVERT_3_IN_3_GGA1(x5)
IF_PLUS_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_PLUS_3_IN_1_GGA1(x4)
CONVERT_3_IN_GGA3(x1, x2, x3)  =  CONVERT_3_IN_GGA2(x1, x2)
IF_CONVERT_3_IN_2_GGA5(x1, x2, x3, x4, x5)  =  IF_CONVERT_3_IN_2_GGA1(x5)
PLUS_3_IN_GGA3(x1, x2, x3)  =  PLUS_3_IN_GGA2(x1, x2)
TIMES_3_IN_GGA3(x1, x2, x3)  =  TIMES_3_IN_GGA2(x1, x2)
IF_CONVERT_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_CONVERT_3_IN_1_GGA2(x2, x4)

We have to consider all (P,R,Pi)-chains

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

CONVERT_3_IN_GGA3(._22(0_0, XS), B, X) -> IF_CONVERT_3_IN_1_GGA4(XS, B, X, convert_3_in_gga3(XS, B, Y))
CONVERT_3_IN_GGA3(._22(0_0, XS), B, X) -> CONVERT_3_IN_GGA3(XS, B, Y)
CONVERT_3_IN_GGA3(._22(s_11(Y), XS), B, s_11(X)) -> IF_CONVERT_3_IN_3_GGA5(Y, XS, B, X, convert_3_in_gga3(._22(Y, XS), B, X))
CONVERT_3_IN_GGA3(._22(s_11(Y), XS), B, s_11(X)) -> CONVERT_3_IN_GGA3(._22(Y, XS), B, X)
IF_CONVERT_3_IN_1_GGA4(XS, B, X, convert_3_out_gga3(XS, B, Y)) -> IF_CONVERT_3_IN_2_GGA5(XS, B, X, Y, times_3_in_gga3(Y, B, X))
IF_CONVERT_3_IN_1_GGA4(XS, B, X, convert_3_out_gga3(XS, B, Y)) -> TIMES_3_IN_GGA3(Y, B, X)
TIMES_3_IN_GGA3(s_11(X), Y, Z) -> IF_TIMES_3_IN_1_GGA4(X, Y, Z, times_3_in_gga3(X, Y, U))
TIMES_3_IN_GGA3(s_11(X), Y, Z) -> TIMES_3_IN_GGA3(X, Y, U)
IF_TIMES_3_IN_1_GGA4(X, Y, Z, times_3_out_gga3(X, Y, U)) -> IF_TIMES_3_IN_2_GGA5(X, Y, Z, U, plus_3_in_gga3(Y, U, Z))
IF_TIMES_3_IN_1_GGA4(X, Y, Z, times_3_out_gga3(X, Y, U)) -> PLUS_3_IN_GGA3(Y, U, Z)
PLUS_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> IF_PLUS_3_IN_1_GGA4(X, Y, Z, plus_3_in_gga3(X, Y, Z))
PLUS_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> PLUS_3_IN_GGA3(X, Y, Z)

The TRS R consists of the following rules:

convert_3_in_gga3([]_0, B, 0_0) -> convert_3_out_gga3([]_0, B, 0_0)
convert_3_in_gga3(._22(0_0, XS), B, X) -> if_convert_3_in_1_gga4(XS, B, X, convert_3_in_gga3(XS, B, Y))
convert_3_in_gga3(._22(s_11(Y), XS), B, s_11(X)) -> if_convert_3_in_3_gga5(Y, XS, B, X, convert_3_in_gga3(._22(Y, XS), B, X))
if_convert_3_in_3_gga5(Y, XS, B, X, convert_3_out_gga3(._22(Y, XS), B, X)) -> convert_3_out_gga3(._22(s_11(Y), XS), B, s_11(X))
if_convert_3_in_1_gga4(XS, B, X, convert_3_out_gga3(XS, B, Y)) -> if_convert_3_in_2_gga5(XS, B, X, Y, times_3_in_gga3(Y, B, X))
times_3_in_gga3(0_0, Y, 0_0) -> times_3_out_gga3(0_0, Y, 0_0)
times_3_in_gga3(s_11(X), Y, Z) -> if_times_3_in_1_gga4(X, Y, Z, times_3_in_gga3(X, Y, U))
if_times_3_in_1_gga4(X, Y, Z, times_3_out_gga3(X, Y, U)) -> if_times_3_in_2_gga5(X, Y, Z, U, plus_3_in_gga3(Y, U, Z))
plus_3_in_gga3(0_0, Y, Y) -> plus_3_out_gga3(0_0, Y, Y)
plus_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_plus_3_in_1_gga4(X, Y, Z, plus_3_in_gga3(X, Y, Z))
if_plus_3_in_1_gga4(X, Y, Z, plus_3_out_gga3(X, Y, Z)) -> plus_3_out_gga3(s_11(X), Y, s_11(Z))
if_times_3_in_2_gga5(X, Y, Z, U, plus_3_out_gga3(Y, U, Z)) -> times_3_out_gga3(s_11(X), Y, Z)
if_convert_3_in_2_gga5(XS, B, X, Y, times_3_out_gga3(Y, B, X)) -> convert_3_out_gga3(._22(0_0, XS), B, X)

The argument filtering Pi contains the following mapping:
convert_3_in_gga3(x1, x2, x3)  =  convert_3_in_gga2(x1, x2)
[]_0  =  []_0
0_0  =  0_0
._22(x1, x2)  =  ._22(x1, x2)
s_11(x1)  =  s_11(x1)
convert_3_out_gga3(x1, x2, x3)  =  convert_3_out_gga1(x3)
if_convert_3_in_1_gga4(x1, x2, x3, x4)  =  if_convert_3_in_1_gga2(x2, x4)
if_convert_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_convert_3_in_3_gga1(x5)
if_convert_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_convert_3_in_2_gga1(x5)
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga2(x2, x4)
if_times_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_2_gga1(x5)
plus_3_in_gga3(x1, x2, x3)  =  plus_3_in_gga2(x1, x2)
plus_3_out_gga3(x1, x2, x3)  =  plus_3_out_gga1(x3)
if_plus_3_in_1_gga4(x1, x2, x3, x4)  =  if_plus_3_in_1_gga1(x4)
IF_TIMES_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_TIMES_3_IN_1_GGA2(x2, x4)
IF_TIMES_3_IN_2_GGA5(x1, x2, x3, x4, x5)  =  IF_TIMES_3_IN_2_GGA1(x5)
IF_CONVERT_3_IN_3_GGA5(x1, x2, x3, x4, x5)  =  IF_CONVERT_3_IN_3_GGA1(x5)
IF_PLUS_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_PLUS_3_IN_1_GGA1(x4)
CONVERT_3_IN_GGA3(x1, x2, x3)  =  CONVERT_3_IN_GGA2(x1, x2)
IF_CONVERT_3_IN_2_GGA5(x1, x2, x3, x4, x5)  =  IF_CONVERT_3_IN_2_GGA1(x5)
PLUS_3_IN_GGA3(x1, x2, x3)  =  PLUS_3_IN_GGA2(x1, x2)
TIMES_3_IN_GGA3(x1, x2, x3)  =  TIMES_3_IN_GGA2(x1, x2)
IF_CONVERT_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_CONVERT_3_IN_1_GGA2(x2, x4)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 3 SCCs with 8 less nodes.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

PLUS_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> PLUS_3_IN_GGA3(X, Y, Z)

The TRS R consists of the following rules:

convert_3_in_gga3([]_0, B, 0_0) -> convert_3_out_gga3([]_0, B, 0_0)
convert_3_in_gga3(._22(0_0, XS), B, X) -> if_convert_3_in_1_gga4(XS, B, X, convert_3_in_gga3(XS, B, Y))
convert_3_in_gga3(._22(s_11(Y), XS), B, s_11(X)) -> if_convert_3_in_3_gga5(Y, XS, B, X, convert_3_in_gga3(._22(Y, XS), B, X))
if_convert_3_in_3_gga5(Y, XS, B, X, convert_3_out_gga3(._22(Y, XS), B, X)) -> convert_3_out_gga3(._22(s_11(Y), XS), B, s_11(X))
if_convert_3_in_1_gga4(XS, B, X, convert_3_out_gga3(XS, B, Y)) -> if_convert_3_in_2_gga5(XS, B, X, Y, times_3_in_gga3(Y, B, X))
times_3_in_gga3(0_0, Y, 0_0) -> times_3_out_gga3(0_0, Y, 0_0)
times_3_in_gga3(s_11(X), Y, Z) -> if_times_3_in_1_gga4(X, Y, Z, times_3_in_gga3(X, Y, U))
if_times_3_in_1_gga4(X, Y, Z, times_3_out_gga3(X, Y, U)) -> if_times_3_in_2_gga5(X, Y, Z, U, plus_3_in_gga3(Y, U, Z))
plus_3_in_gga3(0_0, Y, Y) -> plus_3_out_gga3(0_0, Y, Y)
plus_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_plus_3_in_1_gga4(X, Y, Z, plus_3_in_gga3(X, Y, Z))
if_plus_3_in_1_gga4(X, Y, Z, plus_3_out_gga3(X, Y, Z)) -> plus_3_out_gga3(s_11(X), Y, s_11(Z))
if_times_3_in_2_gga5(X, Y, Z, U, plus_3_out_gga3(Y, U, Z)) -> times_3_out_gga3(s_11(X), Y, Z)
if_convert_3_in_2_gga5(XS, B, X, Y, times_3_out_gga3(Y, B, X)) -> convert_3_out_gga3(._22(0_0, XS), B, X)

The argument filtering Pi contains the following mapping:
convert_3_in_gga3(x1, x2, x3)  =  convert_3_in_gga2(x1, x2)
[]_0  =  []_0
0_0  =  0_0
._22(x1, x2)  =  ._22(x1, x2)
s_11(x1)  =  s_11(x1)
convert_3_out_gga3(x1, x2, x3)  =  convert_3_out_gga1(x3)
if_convert_3_in_1_gga4(x1, x2, x3, x4)  =  if_convert_3_in_1_gga2(x2, x4)
if_convert_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_convert_3_in_3_gga1(x5)
if_convert_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_convert_3_in_2_gga1(x5)
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga2(x2, x4)
if_times_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_2_gga1(x5)
plus_3_in_gga3(x1, x2, x3)  =  plus_3_in_gga2(x1, x2)
plus_3_out_gga3(x1, x2, x3)  =  plus_3_out_gga1(x3)
if_plus_3_in_1_gga4(x1, x2, x3, x4)  =  if_plus_3_in_1_gga1(x4)
PLUS_3_IN_GGA3(x1, x2, x3)  =  PLUS_3_IN_GGA2(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

PLUS_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> PLUS_3_IN_GGA3(X, Y, Z)

R is empty.
The argument filtering Pi contains the following mapping:
s_11(x1)  =  s_11(x1)
PLUS_3_IN_GGA3(x1, x2, x3)  =  PLUS_3_IN_GGA2(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

PLUS_3_IN_GGA2(s_11(X), Y) -> PLUS_3_IN_GGA2(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {PLUS_3_IN_GGA2}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

TIMES_3_IN_GGA3(s_11(X), Y, Z) -> TIMES_3_IN_GGA3(X, Y, U)

The TRS R consists of the following rules:

convert_3_in_gga3([]_0, B, 0_0) -> convert_3_out_gga3([]_0, B, 0_0)
convert_3_in_gga3(._22(0_0, XS), B, X) -> if_convert_3_in_1_gga4(XS, B, X, convert_3_in_gga3(XS, B, Y))
convert_3_in_gga3(._22(s_11(Y), XS), B, s_11(X)) -> if_convert_3_in_3_gga5(Y, XS, B, X, convert_3_in_gga3(._22(Y, XS), B, X))
if_convert_3_in_3_gga5(Y, XS, B, X, convert_3_out_gga3(._22(Y, XS), B, X)) -> convert_3_out_gga3(._22(s_11(Y), XS), B, s_11(X))
if_convert_3_in_1_gga4(XS, B, X, convert_3_out_gga3(XS, B, Y)) -> if_convert_3_in_2_gga5(XS, B, X, Y, times_3_in_gga3(Y, B, X))
times_3_in_gga3(0_0, Y, 0_0) -> times_3_out_gga3(0_0, Y, 0_0)
times_3_in_gga3(s_11(X), Y, Z) -> if_times_3_in_1_gga4(X, Y, Z, times_3_in_gga3(X, Y, U))
if_times_3_in_1_gga4(X, Y, Z, times_3_out_gga3(X, Y, U)) -> if_times_3_in_2_gga5(X, Y, Z, U, plus_3_in_gga3(Y, U, Z))
plus_3_in_gga3(0_0, Y, Y) -> plus_3_out_gga3(0_0, Y, Y)
plus_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_plus_3_in_1_gga4(X, Y, Z, plus_3_in_gga3(X, Y, Z))
if_plus_3_in_1_gga4(X, Y, Z, plus_3_out_gga3(X, Y, Z)) -> plus_3_out_gga3(s_11(X), Y, s_11(Z))
if_times_3_in_2_gga5(X, Y, Z, U, plus_3_out_gga3(Y, U, Z)) -> times_3_out_gga3(s_11(X), Y, Z)
if_convert_3_in_2_gga5(XS, B, X, Y, times_3_out_gga3(Y, B, X)) -> convert_3_out_gga3(._22(0_0, XS), B, X)

The argument filtering Pi contains the following mapping:
convert_3_in_gga3(x1, x2, x3)  =  convert_3_in_gga2(x1, x2)
[]_0  =  []_0
0_0  =  0_0
._22(x1, x2)  =  ._22(x1, x2)
s_11(x1)  =  s_11(x1)
convert_3_out_gga3(x1, x2, x3)  =  convert_3_out_gga1(x3)
if_convert_3_in_1_gga4(x1, x2, x3, x4)  =  if_convert_3_in_1_gga2(x2, x4)
if_convert_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_convert_3_in_3_gga1(x5)
if_convert_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_convert_3_in_2_gga1(x5)
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga2(x2, x4)
if_times_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_2_gga1(x5)
plus_3_in_gga3(x1, x2, x3)  =  plus_3_in_gga2(x1, x2)
plus_3_out_gga3(x1, x2, x3)  =  plus_3_out_gga1(x3)
if_plus_3_in_1_gga4(x1, x2, x3, x4)  =  if_plus_3_in_1_gga1(x4)
TIMES_3_IN_GGA3(x1, x2, x3)  =  TIMES_3_IN_GGA2(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

TIMES_3_IN_GGA3(s_11(X), Y, Z) -> TIMES_3_IN_GGA3(X, Y, U)

R is empty.
The argument filtering Pi contains the following mapping:
s_11(x1)  =  s_11(x1)
TIMES_3_IN_GGA3(x1, x2, x3)  =  TIMES_3_IN_GGA2(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

TIMES_3_IN_GGA2(s_11(X), Y) -> TIMES_3_IN_GGA2(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {TIMES_3_IN_GGA2}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

CONVERT_3_IN_GGA3(._22(0_0, XS), B, X) -> CONVERT_3_IN_GGA3(XS, B, Y)
CONVERT_3_IN_GGA3(._22(s_11(Y), XS), B, s_11(X)) -> CONVERT_3_IN_GGA3(._22(Y, XS), B, X)

The TRS R consists of the following rules:

convert_3_in_gga3([]_0, B, 0_0) -> convert_3_out_gga3([]_0, B, 0_0)
convert_3_in_gga3(._22(0_0, XS), B, X) -> if_convert_3_in_1_gga4(XS, B, X, convert_3_in_gga3(XS, B, Y))
convert_3_in_gga3(._22(s_11(Y), XS), B, s_11(X)) -> if_convert_3_in_3_gga5(Y, XS, B, X, convert_3_in_gga3(._22(Y, XS), B, X))
if_convert_3_in_3_gga5(Y, XS, B, X, convert_3_out_gga3(._22(Y, XS), B, X)) -> convert_3_out_gga3(._22(s_11(Y), XS), B, s_11(X))
if_convert_3_in_1_gga4(XS, B, X, convert_3_out_gga3(XS, B, Y)) -> if_convert_3_in_2_gga5(XS, B, X, Y, times_3_in_gga3(Y, B, X))
times_3_in_gga3(0_0, Y, 0_0) -> times_3_out_gga3(0_0, Y, 0_0)
times_3_in_gga3(s_11(X), Y, Z) -> if_times_3_in_1_gga4(X, Y, Z, times_3_in_gga3(X, Y, U))
if_times_3_in_1_gga4(X, Y, Z, times_3_out_gga3(X, Y, U)) -> if_times_3_in_2_gga5(X, Y, Z, U, plus_3_in_gga3(Y, U, Z))
plus_3_in_gga3(0_0, Y, Y) -> plus_3_out_gga3(0_0, Y, Y)
plus_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_plus_3_in_1_gga4(X, Y, Z, plus_3_in_gga3(X, Y, Z))
if_plus_3_in_1_gga4(X, Y, Z, plus_3_out_gga3(X, Y, Z)) -> plus_3_out_gga3(s_11(X), Y, s_11(Z))
if_times_3_in_2_gga5(X, Y, Z, U, plus_3_out_gga3(Y, U, Z)) -> times_3_out_gga3(s_11(X), Y, Z)
if_convert_3_in_2_gga5(XS, B, X, Y, times_3_out_gga3(Y, B, X)) -> convert_3_out_gga3(._22(0_0, XS), B, X)

The argument filtering Pi contains the following mapping:
convert_3_in_gga3(x1, x2, x3)  =  convert_3_in_gga2(x1, x2)
[]_0  =  []_0
0_0  =  0_0
._22(x1, x2)  =  ._22(x1, x2)
s_11(x1)  =  s_11(x1)
convert_3_out_gga3(x1, x2, x3)  =  convert_3_out_gga1(x3)
if_convert_3_in_1_gga4(x1, x2, x3, x4)  =  if_convert_3_in_1_gga2(x2, x4)
if_convert_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_convert_3_in_3_gga1(x5)
if_convert_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_convert_3_in_2_gga1(x5)
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga2(x2, x4)
if_times_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_2_gga1(x5)
plus_3_in_gga3(x1, x2, x3)  =  plus_3_in_gga2(x1, x2)
plus_3_out_gga3(x1, x2, x3)  =  plus_3_out_gga1(x3)
if_plus_3_in_1_gga4(x1, x2, x3, x4)  =  if_plus_3_in_1_gga1(x4)
CONVERT_3_IN_GGA3(x1, x2, x3)  =  CONVERT_3_IN_GGA2(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

CONVERT_3_IN_GGA3(._22(0_0, XS), B, X) -> CONVERT_3_IN_GGA3(XS, B, Y)
CONVERT_3_IN_GGA3(._22(s_11(Y), XS), B, s_11(X)) -> CONVERT_3_IN_GGA3(._22(Y, XS), B, X)

R is empty.
The argument filtering Pi contains the following mapping:
0_0  =  0_0
._22(x1, x2)  =  ._22(x1, x2)
s_11(x1)  =  s_11(x1)
CONVERT_3_IN_GGA3(x1, x2, x3)  =  CONVERT_3_IN_GGA2(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

CONVERT_3_IN_GGA2(._22(0_0, XS), B) -> CONVERT_3_IN_GGA2(XS, B)
CONVERT_3_IN_GGA2(._22(s_11(Y), XS), B) -> CONVERT_3_IN_GGA2(._22(Y, XS), B)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {CONVERT_3_IN_GGA2}.
We used the following order and afs together with the size-change analysis to show that there are no infinite chains for this DP problem.

Order:Homeomorphic Embedding Order

AFS:
0_0  =  0_0
s_11(x1)  =  s_11(x1)
._22(x1, x2)  =  ._22(x1, x2)

From the DPs we obtained the following set of size-change graphs:

We oriented the following set of usable rules. none